Section: New Results

Formally verified decision procedures for finite automata

Participants : Stephan Merz, Julien Perugini, Hernán Ponce de Leon, Pierre Savonitto.

Decision problems in the theory of finite automata underly verification algorithms in model checking and decision procedures for fragments of arithmetic. We are interested in developing a certified library of automata-theoretic constructions within a trusted interactive proof assistent such as Isabelle. In 2011, two student projects addressed such problems.

Julien Perugini and Pierre Savonitto formalized a decision procedure for the universality problem of finite automata based on the antichain technique suggested by Doyen et al. [27] and verified its correctness in Isabelle/HOL. They then verified a list-based implementation of that algorithm, using the Isabelle Collections Framework, which provides pre-proved data structures for generating executable implementations. Future work should address efficiency issues by adopting better suited data structures.

During his internship, Hernán Ponce de Leon formalized and verified an automaton-based decision procedure for Presburger arithmetic over the integers, based on a previous encoding of a similar procedure restricted to natural numbers.